; COMMAND-LINE: --sygus-inst
; EXPECT: unsat
(set-logic HO_ALL)
(declare-sort u 0)
(declare-fun tptp.funcImageSingleton () Bool)
(declare-fun tptp.func (u u u) Bool)
(declare-fun tptp.in (u u) Bool)
(declare-fun tptp.singleton (u) Bool)
(declare-fun tptp.breln (u u u) Bool)
(declare-fun tptp.dsetconstr (u (-> u Bool)) u)
(declare-fun tptp.emptyset () u)
(declare-fun tptp.setadjoin (u u) u)
(declare-fun tptp.ex1 (u (-> u Bool)) Bool)
(declare-fun tptp.setunion (u) u)
(declare-fun tptp.theprop () Bool)
(declare-fun tptp.cartprod (u u) u)
(declare-fun tptp.dsetconstrEL () Bool)
(declare-fun tptp.subset (u u) Bool)
(declare-fun tptp.kpair (u u) u)
(assert (= tptp.dsetconstrEL (forall ((A u) (Xphi (-> u Bool)) (Xx u)) (let ((_let_1 (@ tptp.in Xx))) (=> (@ _let_1 (@ (@ tptp.dsetconstr A) (lambda ((Xy u)) (@ Xphi Xy)))) (@ _let_1 A))))))
(assert (= tptp.singleton (lambda ((A u)) (exists ((Xx u)) (and (@ (@ tptp.in Xx) A) (= A (@ (@ tptp.setadjoin Xx) tptp.emptyset)))))))
(assert (= tptp.ex1 (lambda ((A u) (Xphi (-> u Bool))) (@ tptp.singleton (@ (@ tptp.dsetconstr A) (lambda ((Xx u)) (@ Xphi Xx)))))))
(assert (= tptp.theprop (forall ((X u)) (=> (@ tptp.singleton X) (@ (@ tptp.in (@ tptp.setunion X)) X)))))
(assert (= tptp.breln (lambda ((A u) (B u) (C u)) (@ (@ tptp.subset C) (@ (@ tptp.cartprod A) B)))))
(assert (= tptp.func (lambda ((A u) (B u) (R u)) (and (@ (@ (@ tptp.breln A) B) R) (forall ((Xx u)) (=> (@ (@ tptp.in Xx) A) (@ (@ tptp.ex1 B) (lambda ((Xy u)) (@ (@ tptp.in (@ (@ tptp.kpair Xx) Xy)) R)))))))))
(assert (= tptp.funcImageSingleton (forall ((A u) (B u) (Xf u)) (=> (@ (@ (@ tptp.func A) B) Xf) (forall ((Xx u)) (=> (@ (@ tptp.in Xx) A) (@ tptp.singleton (@ (@ tptp.dsetconstr B) (lambda ((Xy u)) (@ (@ tptp.in (@ (@ tptp.kpair Xx) Xy)) Xf))))))))))
(assert (not (=> tptp.dsetconstrEL (=> tptp.theprop (=> tptp.funcImageSingleton (forall ((A u) (B u) (Xf u)) (=> (@ (@ (@ tptp.func A) B) Xf) (forall ((Xx u)) (=> (@ (@ tptp.in Xx) A) (@ (@ tptp.in (@ tptp.setunion (@ (@ tptp.dsetconstr B) (lambda ((Xy u)) (@ (@ tptp.in (@ (@ tptp.kpair Xx) Xy)) Xf))))) B))))))))))
(check-sat)

